module TravelDream

abstract sig Data {}
abstract sig Id extends Data {}
sig UserId extends Id {}
sig BaseProductId extends Id {}
sig TravelPackageId extends Id {}
sig Email extends Data {}
sig GenericString extends Data {}
abstract sig Available {}
one sig Yes, No extends Available {}

abstract sig BaseProduct {
	idBaseProduct : one BaseProductId,
	startProductInstant : Int,
	endProductInstant : Int,
	available : one Available,
	basePrice : Int,
	addedInstant : Int
} {
	startProductInstant >= 0
	startProductInstant < endProductInstant
	addedInstant >= 0
   	addedInstant < startProductInstant
	basePrice >= 0
}
sig  Transport extends BaseProduct {}
sig  Hotel extends BaseProduct {}
sig  Excursion extends BaseProduct {}

abstract sig TravelPackage {
	idTravel : one TravelPackageId,
	startTravelInstant : Int,
	endTravelInstant : Int,
	expiryInstant : Int,
	price : Int,
	numParticipants : Int,
	currentBaseProductMaxParticipations : Int,
	madeInstant : Int,
	baseProducts : some BaseProduct
} {
	startTravelInstant >= 0
	startTravelInstant < endTravelInstant
	expiryInstant >= 0
	expiryInstant < startTravelInstant
	numParticipants >= 0
	currentBaseProductMaxParticipations >= 0
	price >= 0
	madeInstant >= 0
	madeInstant < expiryInstant
}
sig PredefinedPackage extends TravelPackage {}
sig CustomPackage extends TravelPackage {}

abstract sig User {
	idUser : one UserId,
	name : GenericString,
	surname : GenericString,
	email : one Email,
	password : one GenericString
}
sig Employee extends User {
	madePackages : set PredefinedPackage,
	addedBaseProducts : set BaseProduct,
	added : one Administrator
}
sig Customer extends User {
	participations : set Participation
}
one sig Administrator extends User {}

sig Participation {
	travelPackage : one TravelPackage,
	participationInstant : Int
} {
	participationInstant >= 0
	participationInstant < travelPackage.expiryInstant
	travelPackage.madeInstant < participationInstant
}

/* Univocità degli id per ogni tipo di entità. */
fact NoDuplicatedIdPerEntity {
	no disj c1, c2 : Customer | c1.idUser = c2.idUser
	no disj e1, e2 : Employee | e1.idUser = e2.idUser
	no disj pp1, pp2 : PredefinedPackage | pp1.idTravel = pp2.idTravel
	no disj cp1, cp2 : CustomPackage | cp1.idTravel = cp2.idTravel
	no disj b1, b2 : BaseProduct | b1.idBaseProduct = b2.idBaseProduct
}

/* Univocità delle email degli utenti. */
fact NoDuplicatedEmailPerUser {
	no disj c1, c2 : Customer | c1.email = c2.email
	no disj e1, e2 : Employee | e1.email = e2.email
	no c : Customer, e : Employee | c.email = e.email
	no c : Customer, a : Administrator | c.email = a.email
	no e :  Employee, a : Administrator | e.email = a.email
}

/* Un pacchetto viaggio è composto da al più due prodotti base trasporto, uno di inizio e
uno di fine viaggio, e gli intervalli temporali dei due non devono intersecarsi. */
fact NoMoreTwoTransports {
	no p : TravelPackage | #(p.baseProducts & Transport) > 2 or
		 (some disj t1, t2 : p.baseProducts | t1 in Transport and  t2 in Transport and
		 t1.endProductInstant > t2.startProductInstant)
}

/* Un pacchetto viaggio è composto da al più un prodotto base hotel. */
fact NoMoreOneHotel {
	no p : TravelPackage | #(p.baseProducts & Hotel) > 1
}

/* L'istante di inizio di un pacchetto viaggio deve coincidere con il minimo istante di inizio di uno
dei suoi prodotti base. */
fact StartTravelEqualMinStartBaseProduct {
	all p : TravelPackage |
	     let baseProducts = p.baseProducts | {
			  one bp : baseProducts | p.startTravelInstant = bp.startProductInstant and
	     	  no bp' : baseProducts | bp' != bp and bp'.startProductInstant < bp.startProductInstant
	     }
}

/* L'istante di fine di un pacchetto viaggio deve coincidere con il massimo istante di fine di uno
dei suoi prodotti base. */
fact EndTravelEqualMaxEndBaseProduct {
	all p : TravelPackage |
	     let baseProducts = p.baseProducts | {
			  one bp : baseProducts | p.endTravelInstant = bp.endProductInstant and
	     	  no bp' : baseProducts | bp' != bp and bp'.endProductInstant > bp.endProductInstant
	     }
}

/* Il prezzo di un pacchetto viaggio deve essere almeno pari alla somma dei prezzi dei suoi prodotti base. */
fact TravelPriceGreaterOrEqualBaseProductPricesSum {
	all p : TravelPackage |
		 let baseProductPricesSum = (sum bp : p.baseProducts | bp.basePrice) | {
		      p.price >= baseProductPricesSum
         }
}

/* Non esiste un pacchetto viaggio con un numero di partecipanti maggiore di zero e 
senza neanche una partecipazione associata. */
fact NoParticipantionsToPartecipatedTravelPackage {
	no tp : TravelPackage | tp.numParticipants > 0 and no p : Participation | p.travelPackage = tp
}

/* Non esistono due o più partecipazioni di un cliente ad uno stesso pacchetto viaggio. */
fact NoMoreCustomerParticipationForSameTravelPackage {
	no c : Customer | some disj p1, p2 : c.participations | p1.travelPackage = p2.travelPackage
}

/* Non esiste una partecipazione associata a più clienti. */
fact NoParticipationToMultipleCustomer {
	all p : Participation | one c : Customer | p in c.participations
}

/* Considerando che il cliente può inserire il numero di prenotazioni per un pacchetto viaggio, le
partecipazioni ad esso associate sono al più pari al numero dei suoi partecipanti. */
fact NoParticipantsLessParticipations {
	no tp : TravelPackage | tp.numParticipants < #(tp.~travelPackage)
}

/* Per ogni pacchetto personalizzato deve esistere almeno un pacchetto predefinito da cui è iniziata
la personalizzazione. I due pacchetti viaggio hanno la stessa scadenza, e il pacchetto personalizzato ha
un istante di creazione maggiore di quello predefinito. */
fact CustomPackageReferredToBasePredefinedPackage {
	all cp : CustomPackage | some pp : PredefinedPackage | cp.expiryInstant = pp.expiryInstant and
		 cp.madeInstant > pp.madeInstant
}

/* La conferma di un pacchetto personalizzato da parte del cliente implica la sua partecipazione, e quindi
avrà un numero di partecipanti almeno pari a uno. */
fact SomeParticipantsToCustomPackage {
	all cp : CustomPackage |  cp.numParticipants > 0 and some c : Customer, p : Participation |
		 p.travelPackage = cp and p in c.participations
}

/* Non esiste un prodotto base senza un impiegato che lo abbia aggiunto. */
fact NoBaseProductWithoutEmployee {
	no bp : BaseProduct | all e : Employee |  bp not in e.addedBaseProducts
}

/* Se un prodotto base fa parte di un pacchetto viaggio, l'istante della sua aggiunta nel sistema
deve essere minore o uguale alla data di creazione del pacchetto viaggio. */
fact NoAddedBaseProductInstantLessMadeTravelPackageInstant {
	no bp : BaseProduct | some tp : TravelPackage | bp in tp.baseProducts and
		 bp.addedInstant > tp.madeInstant
}

/* Ogni pacchetto viaggio che ha un numero massimo di partecipazioni corrente maggiore
di zero, ha i prodotti base tutti disponibile. */
fact TravelPackageCurrentMaxParticipationsGreaterZeroIffAllBaseProductsAvailable {
	all tp : TravelPackage | tp.currentBaseProductMaxParticipations > 0 iff all bp : tp.baseProducts |
		 bp.available = Yes
}

/* Non esiste un prodotto base non disponibile senza un pacchetto viaggio con una
o più partecipazioni. */
fact NoBaseProductNotAvailableWithoutTravelPackageParticipations {
	no bp : BaseProduct | bp.available = No and all tp : TravelPackage | bp not in tp.baseProducts or
	(bp in tp.baseProducts and no p : Participation | p.travelPackage = tp)
}

/* Il numero massimo di partecipazioni corrente è pari al minimo tra le disponibilità correnti dei
prodotti base. */
fact DifferentCurrentMaxParticipations {
	all disj tp, tp' : TravelPackage |
		 #(tp.baseProducts & tp'.baseProducts) > 0 implies
	     (tp.currentBaseProductMaxParticipations = tp'.currentBaseProductMaxParticipations iff
		 (no tp'' : TravelPackage | tp'' != tp' and tp'' != tp and #(tp.baseProducts & tp''.baseProducts) > 0 and
		 tp''.currentBaseProductMaxParticipations < tp'.currentBaseProductMaxParticipations))
}

/* Se c'è disponibilità, il cliente partecipa e conferma le prenotazioni ad un pacchetto viaggio.
Il cliente può confermare più di una volta e in momenti diversi, aumentando il numero di prenotazioni. */
pred ConfirmParticipation(t, t' : TravelPackage, reservations : Int, instant : Int) {
	reservations > 0 and (all bp : t.baseProducts | bp.available = Yes) and
	reservations <= t.currentBaseProductMaxParticipations and instant < t.expiryInstant and
	((t in PredefinedPackage and t' in PredefinedPackage) or
	(t in CustomPackage and t' in CustomPackage)) and t'.startTravelInstant = t.startTravelInstant
	and t'.endTravelInstant = t.endTravelInstant and t'.expiryInstant = t.expiryInstant and
	t'.price = t.price and t'.numParticipants = add[t.numParticipants, reservations] and
	t'.currentBaseProductMaxParticipations = t.currentBaseProductMaxParticipations and
	t'.madeInstant = t.madeInstant and t'.baseProducts = t.baseProducts and
	one p : t.~travelPackage, p' : t'.~travelPackage | p.participationInstant < p'.participationInstant
}
run ConfirmParticipation for 10

pred show {}
run show for 7

/* Non esistono pacchetti viaggio con alcuni prodotti base disponibili e altri no, ma che permettono
la partecipazione. */
assert NoTravelPacketAvailableWithBaseProductNotAvailable {
	no tp : TravelPackage | some bp1, bp2 : tp.baseProducts | bp1.available = No and
		 bp2.available = Yes and tp.currentBaseProductMaxParticipations > 0
}
check NoTravelPacketAvailableWithBaseProductNotAvailable for 10

/* Non esiste un pacchetto personalizzato senza neanche una partecipazione. */
assert NoPartecipationsForCustomPackage {
	no cp : CustomPackage | #(Participation.travelPackage & cp) = 0
}
check NoPartecipationsForCustomPackage for 10

/* Non esiste un prodotto base con istante di inizio minore all'istante di inizio di un
qualche pacchetto che lo contiene. Non esiste un prodotto base con istante di fine maggiore
all'istante di fine di un qualche pacchetto che lo contiene. */
assert NoExternBaseProductIntervalFromTravelPackageInterval {
	no bp : BaseProduct | some tp : TravelPackage | bp in tp.baseProducts and
			  (bp.startProductInstant < tp.startTravelInstant or
			  bp.endProductInstant > tp.endTravelInstant)
}
check NoExternBaseProductIntervalFromTravelPackageInterval for 10
